TIMEOUT We are left with following problem, upon which TcT provides the certificate TIMEOUT. Strict Trs: { >(s(x), s(y)) -> >(x, y) , >(s(x), 0()) -> true() , >(0(), s(y)) -> false() , >(0(), 0()) -> false() , quicksort(nil()) -> nil() , quicksort(::(z, zs)) -> quicksort'(z, split(z, zs)) , split(pivot, nil()) -> pair(nil(), nil()) , split(pivot, ::(x, xs)) -> split'(>(x, pivot), x, split(pivot, xs)) , quicksort'(z, pair(xs, ys)) -> append(quicksort(xs), ::(z, quicksort(ys))) , append(nil(), ys) -> ys , append(::(x, xs), ys) -> ::(x, append(xs, ys)) , split'(true(), x, pair(ls, rs)) -> pair(ls, ::(x, rs)) , split'(false(), x, pair(ls, rs)) -> pair(::(x, ls), rs) } Obligation: runtime complexity Answer: TIMEOUT Computation stopped due to timeout after 300.0 seconds. Arrrr..